;;;============================================================================
;;;
;;; Subject: Representation of a lists as strictly increasing lists of
;;;          natural numbers and its relation with binary lists
;;;          
;;;
;;;----------------------------------------------------------------------------
;;;
;;; JHV 01-03-10
;;;
;;;============================================================================

#| To certify this book:

(certify-book "increasing-list" 0 nil)

|#

(in-package "ACL2")

(set-verify-guards-eagerness 0)


;;;----------------------------------------------------------------------------
;;;
;;; Characterization function
;;;
;;;----------------------------------------------------------------------------

(defun increasing-p (dgl)
  (if (endp dgl)
      (equal dgl nil)		
      (if (endp (cdr dgl))
	  (and (equal (cdr dgl) nil)
	       (natp (car dgl)))
	  (and (natp (car dgl))
	       (natp (cadr dgl))
	       (< (car dgl) (cadr dgl))
	       (increasing-p (cdr dgl))))))


;;;----------------------------------------------------------------------------
;;;
;;; Transformation functions to lists domain
;;;
;;;----------------------------------------------------------------------------

;; (1 3 4 6) -> (0 1 0 1 1 0 1)
;;                 ^   ^ ^   ^
;;                 1   3 4   6

(defun dgb-pos (n)
  (cond ((zp n) '(1))
	(t (cons 0 (dgb-pos (- n 1))))))

(defun dgb-app (dgb1 dgb2)
  (cond ((endp dgb1) dgb2)
	((endp dgb2) dgb1)
	(t (cons (car dgb1) (dgb-app (cdr dgb1) (cdr dgb2))))))

(defun increasing->dgb (dgl)
  (cond ((endp dgl) nil)
	(t (dgb-app (dgb-pos (car dgl)) 
		    (increasing->dgb (cdr dgl))))))

; (increasing->dgb '(1 3 4 6)) -> (0 1 0 1 1 0 1)
; (increasing->dgb '(0 1 3 5)) -> (1 1 0 1 0 1)
; (increasing->dgb '()) -> nil

;;;----------------------------------------------------------------------------

(defun 1+ls (lst)
  (cond ((endp lst) nil)
	(t (cons (1+ (car lst))
		 (1+ls (cdr lst))))))

(defun dgb->increasing (dgb)
  (cond ((endp dgb) nil)
	((eql (car dgb) 0) (1+ls (dgb->increasing (cdr dgb))))
	(t (append (list 0) (1+ls (dgb->increasing (cdr dgb)))))))
	 
; (dgb->increasing '(1 0 1)) -> (0 2)
; (dgb->increasing '(0 1 0 1 1 0 1)) -> (1 3 4 6)
; (dgb->increasing '(1 1 0 1 0 1)) -> (0 1 3 5)
; (dgb->increasing '(0 1 1 0 1)) -> (1 2 4)
; (dgb->increasing '()) -> nil

;;;============================================================================
;;;
;;; Properties
;;;
;;;============================================================================

(include-book "dg-binary")

;;;----------------------------------------------------------------------------
;;;
;;; Preliminaries
;;;
;;;----------------------------------------------------------------------------

(encapsulate
 ()

 (local
  (defthm commutativity-2-of-+-lemma
    (equal (+ (+ x y) z)
	   (+ (+ y x) z))
     :rule-classes nil))

 (defthm commutativity-2-of-+
    (equal (+ x (+ y z))
	   (+ y (+ x z)))
    :hints (("Goal"
	     :in-theory (disable commutativity-of-+)
	     :use commutativity-2-of-+-lemma))))

;;;----------------------------------------------------------------------------
;;;
;;; Domain properties
;;;
;;;----------------------------------------------------------------------------

(defthm dgb-p-increasing->dgb
  (implies (increasing-p dgl)
	   (dgb-p (increasing->dgb dgl))))

;;;----------------------------------------------------------------------------

(defthm increasingp-1+ls-increasingp
  (implies (increasing-p ls)
	   (increasing-p (1+ls ls))))

(defthm natp-car-increasing-p
  (implies (and (consp ls)
		(increasing-p ls))
	   (natp (car ls))))

(defthm car-1+ls-increasing-p
  (implies (and (consp ls)
		(increasing-p ls))		
	   (< 0 (car (1+ls ls))))
  :rule-classes :linear)

(defthm increasing-p-dgb->increasing
  (implies (dgb-p dgb)
	   (increasing-p (dgb->increasing dgb)))
  :hints (("Subgoal *1/5.2" 
	   :use ((:instance increasingp-1+ls-increasingp
			   (ls (dgb->increasing (cdr dgb))))
		 (:instance car-1+ls-increasing-p
			   (ls (dgb->increasing (cdr dgb))))))))

;;;----------------------------------------------------------------------------
;;;
;;; Composition of transformations
;;;
;;;----------------------------------------------------------------------------

(defthm increasing->dgb-1+ls
  (implies (and (increasing-p dgl)
		(consp dgl))
	   (equal (increasing->dgb (1+ls dgl))
		  (cons 0 (increasing->dgb dgl)))))

(defthm increasing->dgb-append-1+ls
  (implies (increasing-p dgl)
	   (equal (increasing->dgb (append '(0) (1+ls dgl) ))
		  (cons 1 (increasing->dgb dgl)))))

(defthm cdr-increasing
  (implies (increasing-p dgl)
	   (equal (cdr (increasing->dgb (1+ls dgl)))
		  (increasing->dgb dgl))))

(defthm increasing->dgb-dgb->increasing
  (implies (dgb-p dgb)
	   (equal (increasing->dgb (dgb->increasing dgb))
		  dgb))
  :hints (("Subgoal *1/3''" :use
	   ((:instance increasing->dgb-1+ls
		       (dgl (DGB->INCREASING (CDR DGB))))))))
;;;----------------------------------------------------------------------------

(defthm dgb->increasing-dgb-pos
  (implies (natp n)
	   (equal (dgb->increasing (dgb-pos n))
		  (list n))))




(defthm dgb->increasing-dgb-app
  (implies (and (dgb-p dgb1)
		(dgb-p dgb2)
		(dgb< dgb1 dgb2))
	   (equal (dgb->increasing (dgb-app dgb1 dgb2))
		  (append (dgb->increasing dgb1)
			  (dgb->increasing dgb2)))))

(defun dgb< (dgb1 dgb2)
  (cond ((endp dgb1) t)
	((endp dgb2) nil)
	(t (and (eql (car dgb2) 0)
		(dgb< (cdr dgb1) (cdr dgb2))))))

(defthm cdr-dgb-pos
  (implies (and (natp n)
		(< 0 n))
	   (equal (cdr (dgb-pos n))
		  (dgb-pos (- n 1)))))

(defthm car-dgb-pos
  (implies (and (natp n)
		(< 0 n))
	   (equal (car (dgb-pos n)) 0)))

(defun natp-induct-2 (n m)
  (if (or (zp n) (zp m))
      t
      (natp-induct-2 (- n 1) (- m 1))))

(defthm dgb<-dgb-pos-n-m
  (implies (and (natp n)
		(natp m)
		(< m n))
	   (dgb< (dgb-pos m) (dgb-pos n)))
  :hints (("Goal" :induct (natp-induct-2 m n))))

(defthm dgb<-dgb-app-alt
  (implies (and (dgb-p dgb1)
		(dgb-p dgb2)
		(dgb-p dgb3)
		(dgb< dgb1 dgb2)
		(dgb< dgb1 dgb3))
	   (dgb< dgb1 (dgb-app dgb2 dgb3))))

(defthm dgb<-increasing->dgb-dgb-pos
  (implies (and (increasing-p (cons n dgl))
		(consp dgl))
	   (dgb< (dgb-pos n)
		 (increasing->dgb dgl)		 
		 ))
:hints (("Goal" :induct (increasing->dgb dgl))))

(defthm dgb->increasing-increasing->dgb
  (implies (increasing-p dgl)
	   (equal (dgb->increasing (increasing->dgb dgl))
		  dgl)))


;;;----------------------------------------------------------------------------
;;;
;;; Remove final zeros properties
;;;
;;;----------------------------------------------------------------------------

(include-book "binary-remove-zeros")

(encapsulate 
 ()
 
(local (defthm 1+ls-dgb->increasing
  (equal (1+ls (dgb->increasing dgb))
	 (dgb->increasing (cons 0 dgb)))))


(local (defthm cons-0-my-reverse
  (equal (cons 0 (my-reverse a))
	 (my-reverse (append a '(0))))))

(local (defthm append-remove-initial
  (implies (and (quasi-dgb-p a)
		(not (all-zeros-p a)))
  (equal (append (remove-initial-zeros a) '(0))
	 (remove-initial-zeros (append a '(0)))))))



(local (defthm dgb->increasing-remove-all-zeros-p-help
  (implies (all-zeros-p dgop)
	   (equal (remove-final-zeros dgop)
		  nil))))


(local (defthm dgb->increasing-remove-all-zeros-p
  (implies (all-zeros-p dgop)
	   (equal (dgb->increasing (remove-final-zeros dgop))
		  nil))
  :hints (("Goal" :use
	   ((:instance dgb->increasing-remove-all-zeros-p-help)))))
       )

(local (defthm dgb->increasing-all-zeros-p
  (implies (all-zeros-p dgop)
	   (equal (dgb->increasing dgop)
		  nil))))


(local (defthm dgb->increasing-remove-final-zeros-help1
  (implies (and (quasi-dgb-p dgop)
		(all-zeros-p dgop))
	   (equal (dgb->increasing dgop)
		  (dgb->increasing (remove-final-zeros dgop))))
  :hints (("Goal" :use
	   ((:instance dgb->increasing-remove-all-zeros-p))))))


(local (defthm all-zeros-p-my-reverse-remove-reverse
 (implies (all-zeros-p dgop)
	  (equal (MY-REVERSE (REMOVE-INITIAL-ZEROS (MY-REVERSE dgop)))
		 nil))))

(local (defthm not-all-zeros-my-reverse-not-all-zeros
  (implies (and (not (all-zeros-p dgop))
		(quasi-dgb-p dgop))
	   (not (all-zeros-p (my-reverse dgop))))))
 
(local (defthm my-reverse-quasi-dgb-p
  (implies (quasi-dgb-p a)
	   (quasi-dgb-p (my-reverse a)))))
       

(local (defthm 1+ls-a-b
  (implies (equal a b)
	   (equal (1+ls a) (1+ls b)
		  ))
  :rule-classes nil))


(local (defthm dgb->increasing-remove-final-zeros-help2-aux
  (implies (and (quasi-dgb-p dgop)
		(not (all-zeros-p dgop))
		(equal (dgb->increasing dgop)
		       (dgb->increasing (my-reverse (remove-initial-zeros
						     (my-reverse dgop))))))
	   (equal (1+ls (dgb->increasing dgop))
		  (dgb->increasing (my-reverse (remove-initial-zeros (append
						     (my-reverse dgop) '(0)))))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-initial-zeros-append-0)
	   :use
	   ((:instance 1+ls-a-b
		       (a (dgb->increasing dgop))
		       (b (dgb->increasing (my-reverse (remove-initial-zeros
						     (my-reverse dgop))))))
	    (:instance 1+ls-dgb->increasing (dgb dgop))
	    (:instance cons-0-my-reverse (a (remove-initial-zeros (my-reverse dgop))))
	    (:instance not-all-zeros-my-reverse-not-all-zeros)
	    (:instance my-reverse-quasi-dgb-p)
	    (:instance append-remove-initial (a (my-reverse dgop)))))
)))




(local (defthm dgb->increasing-remove-final-zeros-help2
  (implies (and (quasi-dgb-p dgop)
		(not (all-zeros-p dgop)))
	   (equal (dgb->increasing dgop)
		  (dgb->increasing (remove-final-zeros dgop))))
  :hints (("Goal" :in-theory (disable remove-initial-zeros-append-0))
	  )))

(defthm dgb->increasing-remove-final-zeros
  (implies (quasi-dgb-p dgop)
	   (equal (dgb->increasing dgop)
		  (dgb->increasing (remove-final-zeros dgop))))
  :hints (("Goal" :do-not-induct t
	   :use 
	   ((:instance dgb->increasing-remove-final-zeros-help2)
	    (:instance dgb->increasing-remove-final-zeros-help1)
	    )))
)

)